
(**
   Homework 1: Types and Terms
 *) 

module Hw1 : Hw1 =
struct 

(**
   Enter the following as HOL Light types
 *)

(* 1. The boolean type. *) 

let t1 = `:a`

(* 2. The type of natural numbers. *)

let t2 = `:a`

(* 3. The type of real numbers. *)

let t3 = `:a`

(* 4. The type of integers. *)

let t4 = `:a`

(* 5. The type of an ordered pair whose components are both natural numbers. *)

let t5 = `:a`

(* 6. The type of a function whose domain is natural numbers and range is real. *)

let t6 = `:a`

(* 7. The type of a set of real numbers. *)

let t7 = `:a`

(* 8. The type of a set of natural numbers. *)

let t8 = `:a`

(* 9. The type of a family of sets, such that each set in the
   family contains natural numbers. *)

let t9 = `:a`

(* 10.  The type of the powerset of the set of real numbers. *)

let t10 = `:a`

(**
   Enter the following as HOL Light terms.  Do not worry about explicit type
   annotations.  (ignore the "Inventing type variables" warning)
 *)

(* 1. true *)

let p1 = `0`;;

(* 2. false *)

let p2 = `0`;;

(* 3. P implies Q. *)

let p3 = `0`;;

(* 4. P if and only if Q. *)

let p4 = `0`;;

(* 5. not P. *)

let p5 = `0`;;

(* 6. Not P implies Q. *)

let p6 = `0`;;

(* 7. false implies P. *)

let p7 = `0`;;

(* 8. P implies a contradiction. *)

let p8 = `0`;;

(* 9. (true implies P) iff P. *)

let p9 = `0`;;

(* 10. P implies Q if and only if not Q implies not P. *)

let p10 = `0`;;

(* 11. For all real x, x^2 >= 0. *)

let p11 = `0`;;

(* 12. For every real number y, there exists a natural number m such that y < m. *)

let p12 = `0`;;

(* 13. The set of real numbers X is not empty. *)

let p13 = `0`;;

(* 14. There exists a set of real numbers X that is empty. *)

let p14 = `0`;;

(* 15. f(x) is greater than g(y) as real numbers.  x and y are real as well. *)

let p15 = `0`;;

(* 16. If x = y then f(x) = f (y).  x, y and f(x) are all real numbers.  *)

let p16 = `0`;;

(* 17. 1/2 is between 0 and 1 as real numbers. *)

let p17 = `0`;;

(* 18. f is an injective function from R to R. (Write out the deﬁning property.) *)

let p18 = `0`;;

(* 19. f is a surjective function from R to R. (Write out the deﬁning property.) *)

let p19 = `0`;;

(* 20. For every positive epsilon, there exists a delta (depending on epsilon)
   such that if |x−y| < epsilon then |f (x) − f (y)| < delta. *)

let p20 = `0`;;

(* 21. A is a subset of B. *)

let p21 = `0`;;

(* 22. The intersection of A and B is C. *)

let p22 = `0`;;

(* 23. The union of A and B is C. *)

let p23 = `0`;;

(* 24. The intersection of A and B is equal to the intersection of B and A. *)

let p24 = `0`;;

(* 25. The union of A and B is a subset of C. *)

let p25 = `0`;;

(* 26. There exists a power of 2 that is greater than 17. *)

let p26 = `0`;;

(* 27. There exists a power of 2 that is greater than 77.7. *)

let p27 = `0`;;

(* 28. 3 − 4 = −1 (as integers). *)

let p28 = `0`;;

(* 29. 3 − 4 = −1 (as real numbers). *)

let p29 = `0`;;

(* 30. −(−4) + 3 − 7. *)

let p30 = `0`;;

(* 31. 3 + (−4). *)

let p31 = `0`;;

(* 1/0. *)

let p32 = `0`;;

(* 33. The union of the family of sets X is C. *)

let p33 = `0`;;

(* 34. The empty set {}. *)

let p34 = `0`;;

(* The singleton set {x}. *)

let p35 = `0`;;

(* The ordered pair (1, 2). *)

let p36 = `0`;;

(* The set {1, 2, 3}. *)

let p37 = `0`;;

(* The set {1, 2, 3} has three elements. *)

let p38 = `0`;;

(** 
  Enter the following as HOL Light terms with the given types. 
  You may need type annotations.  (You should not get the 
  "inventing type variables" warning.)
 *) 

(* 1. The term X of type A. *)

let h1 = `0`

(* 2. x is a real number. *)

let h2 = `0`

(* 3. X has the type of a subset of the real numbers. *)

let h3 = `0`

(* 4. X is equal to the set of real numbers. *)

let h4 = `0`

(* 5. v ∈ R3 . *)

let h5 = `0`

(* 6. v + w, where v, w ∈ R3 . *)

let h6 = `0`

(* 7. X has the type of a collection of subsets of the real numbers. *)

let h7 = `0`

(* 8. −v, where v ∈ R3 . *)

let h8 = `0`

(* 9. The third component of v ∈ R3 . *)

let h9 = `0`

(* 10. The scalar multiple 3v, where v ∈ R3 . *)

let h10 = `0`

(* 11. The dot product v · w of two vectors in R3 . *)

let h11 = `0`

(* 12. The combination 2v + 4w − 7u in R3 . *)

let h12 = `0`

end
